Nuprl Lemma : empty_support
4,23
postcript
pdf
n
:
,
f
:(
n
). (
x
:
n
.
f
(
x
) = 0)
sum(
f
(
x
) |
x
<
n
) = 0
latex
Definitions
A
B
,
A
,
False
,
P
Q
,
sum(
f
(
x
) |
x
<
k
)
,
x
(
s
)
,
{
i
..
j
}
,
x
:
A
.
B
(
x
)
,
t
T
,
,
Prop
,
SQType(
T
)
,
{
T
}
,
x
.
t
(
x
)
,
P
Q
,
P
&
Q
,
P
Q
Lemmas
sum
constant
,
sum
functionality
,
sum
wf
,
nat
wf
,
int
seg
wf
origin
n:
, f:(n
). (x:n. f(x) = 0) 
sum(f(x) | x < n) = 0 n:, f:(n). (x:n. f(x) = 0) sum(f(x) | x < n) = 0 
B
A Q
}x:A. B(x)
T
x. t(x)
Q Q